Nuprl Lemma : tree_leaf_wf2
4,23
postcript
pdf
E
:Type,
x
:
E
. tree_leaf(
x
)
Tree(
E
)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
S
T
,
tree_leaf(
x
)
,
Tree(
E
)
Lemmas
tree
wf
,
tree
leaf
wf
,
tree
subtype2
origin
E:Type, x:E. tree_leaf(x) 
Tree(E) E:Type, x:E. tree_leaf(x) Tree(E) x:A. B(x) T
T